Recently, a system has been revised or a revised edition of a system has been published frequently, caused by missing verification of a corner case due to the complexity of a circuit and an increase of circuit size of a semiconductor integrated circuit, by missing confirmation of interface specifications among blocks allocated to plural designers due to group work, or by specification errors of a reusable core purchased from a third party.
These problems come from, for example, insufficient circuit verification or a test scenario that can extract bugs, which were not able to be formed because a corner case and core specifications of the third party were not understood sufficiently.
In order to solve these problems, an assertion verification technology, in which a property with respect to circuit specifications is converted into an assertion description and the assertion description is input to a simulator (computer) for verification, and a function coverage report for showing a warning for assertion violation during the simulation and showing whether a specific circuit sequence has been tested by a simulator is given, has been proposed and has been recently put into use in actual designing.
An assertion is a note in which intention (in some cases, this shows property) of designing is written and is generally written by a comment sentence in a RTL. The intention is interpreted by a simulator during the verification, for example, an error log is generated in a case where a circuit to be verified operates differently from the intention. The intention of designing is, for example, an assumption and a precondition of circuit input, and in addition to these, expected operations when the conditions are satisfied.
The simulator checks the following two matters.
(1) Specific events such as an assumption and a precondition have occurred.
(2) Expected operations at that time complete normally.
From the above check (1), the assertion gives feedback of determining information as to whether a specific circuit function is confirmed by verification. Therefore, when the assertion is comprehensively installed in a circuit to be verified, function coverage of the assertion can be obtained; consequently, its verification accuracy can be obtained quantitatively.
From the above check (2), the feedback to a verification debugging can be obtained by the assertion. For example, an assertion installed in a position, from which an influence caused by a circuit malfunction cannot be observed by external terminals, complements a malfunction state. In addition, when conditions such as an assumption and a precondition are satisfied in any stimulus, this expected operation is checked at any time. Therefore, for example, even when the stimulus is structured by a random system, self-collation with the expected operation, that is, comparison of expected values, can be executed. In addition, an assertion installed in a lower block is also effective in chip level verification.
The intention of designing may be described by a Verilog-HDL for verification being different from a RTL for logic synthesis; however, here, another assertion language is described.
At present, the most popular assertion language is a PSL (property specification language) described in Non-Patent Document 1. The PSL is an assertion language which will be given to IEEE from a standardization organization named Accellera, and is actually a standard language. In the following, an actual example of an assertion description using the PSL is shown.
For example, it is assumed that the following design intention (property) for memory control is desired to monitored by verification.    1) read_n and write_n do not become Low at the same time    2) at the fall (negative) of write_n, enable_n is High    3) at the fall of read_n, enable_n is Low
The PSL description (assertion description) to be given to a simulator as an assertion for the intention is as follows.    // psl property memcont1=never (!write_n && !read_n) @(posedge clk);    // psl assert memcont1;    // psl property memcont2=always (enable_n) @(negedge write_n);    // psl assert memcont2;    // psl property memcont3=always (!enable_n) @(negedge read_n);    // psl assert memcont3;
All of “psl, property, never, assert, always” in the above PSL description (assertion description) are reserved words in the PSL. All rows start with “//” which shows a comment of the Verilog-HDL. In this, instead of using “//”, all of the PSL descriptions can be closed with “/**/”.
The words “memcont1,2,3, !write_n && !read_n, posedge clk, enable_n, negedge write_n, !enable_n, negedge read_n” are descriptions by a user definition, and actual installed data names, that is, memory control signal names which appear in the RTL for defining the intention of 1) through 3) except for “memcont1,2,3”.
In addition, “memcont1 though 3” are assertion names and are used for knowing an error log and a function coverage being given from the simulator as feedback.
The assertion description by the PSL has the following structural elements.    // psl property <an assertion name>=
<an event to be monitored> -> <expected operation when a condition is satisfied> @<a strobe condition>;    // psl assert <an assertion name>;
For example, in the assertion description of 1), “memcont1” is an assertion name, “!write_n && !read_n” is an event to be monitored, in this case, “never” is added in front of the event; therefore, it is monitored that the condition (event) in ( ) never becomes true. If “always” is added, it is monitored that the condition in ( ) is true. In addition, by “@(posedge clk)” which follows the above statement, it is defined that monitoring the condition is executed at every time of rising edges (positive edges). “->” changes to “|=>” or “|->” depending on the time when the expected operation is started. In this, the above example does not accompany expected operations.
The part in ( ) except the strobe condition is described by the Verilog-HDL which returns Boolean values. The part in ( ) of the strobe condition has a description form of a sensitivity list described by an “always sentence” of the Verilog-HDL.
In the PSL, an event to be monitored can be defined, and each part of expected operations at the time when the condition is satisfied can define a sequence, that is, the changes of events and expected operations in plural cycles can be defined. An example is explained.
The intention of designing: When a clear start condition (m_task==2′ 00) is satisfied in a clearing process of a memory, in order to initialize all words (256 words), a writing operation is repeated 256 times. Here, one writing operation is completed by the operation of Low→High→High of write_n synchronized with a rise cycle (positive cycle) of clk.
The PSL description:    // psl sequence WRITE_PULSE={!write_n; write_n; write_n };    // psl property CLEAR_MEM_WRITE_N=    // always {m_task==2′ b00} |=> {WRITE_PULSE [*256]}    // @(posedge clk);    // psl assert CLEAR_MEM_WRITE_N;
“sequence” defines a Low→High→High sequence of “write_n” by a macro-definition.
Here, it is the part of expected operations which follows “|=>” that is to be focused on. When “m_task==2′ boo”, the expected operation is WRITE_PULSE, that is, it is expected that the sequence of Low→High→High being three cycles of write_n be repeated by 256 times.
However, in such an assertion verifying technology, for example, in a case where the assertion description language is written by a manual input when the specifications are defined, there is a possibility that a mistake may be made in the assertion itself. As a result, a report of the warning of the assertion violation and the function coverage obtained by the assertion verification cannot be fed back to prevent the system revision and the revised edition of the system. Further, this requires a verification period for debugging the assertion description language. Consequently, the verification efficiency becomes worse.
In other words, the major premise of the assertion verifying technology is that the circuit specifications and the assertion description match each other; however, there is no method to confirm the matching before executing the simulation. Further, with respect to a complex finite state machine, it is difficult to describe a sequence of a comprehensive state transition by manual operation.
As conventional technologies with respect to the assertion verification, for example, there are technologies disclosed in Patent Document 1 and Patent Document 2.
In Patent Document 1, a technology, in which a state transition machine is modeled by a graph and a state transition path that satisfies the assertion is searched, is disclosed. Further, a technology to confirm the rightness of the assertion by only an analysis of this graph is disclosed. By the technologies, matching the circuit specifications with the assertion description can be confirmed.
However, in these technologies, with respect to the state transition machine which is made to be a graph, a model of the state transition machine which becomes a basic model is formed manually, or the state transition machine is extracted from design data formed by a description language of a RTL. Consequently, mixing a mistake in an object to be matched, that is, in the model of the state transition machine which should be the circuit specifications, cannot be avoided.
In addition, in Patent Document 2, a technology, which generates an assertion for verifying a circuit by extracting a data transfer structure from design data of a RTL and expanding the data transfer structure into a graphic structure, is disclosed. However, in this technology, since the assertion which is the circuit specifications is extracted from the design data, matching the circuit specifications with the assertion description cannot be assured.
[Patent Document 1] Japanese Laid-Open Patent Application No. 2000-181933
[Patent Document 2] Japanese Laid-Open Patent Application No. 2000-142918
[Non-Patent Document 1] Property Specification Language Reference Manual Version 1.1 Jun. 9, 2004, online, retrieved in Sep. 14, 2004, from the Internet, URL: http://www.eda.org/vfv/docs/PSL-v1.1.pdf
Consequently, in the conventional technologies, matching the circuit specifications with the assertion description cannot be assured.